*****************************************************************
YQF from equivalential calculus

(define mp
  {--> prop}
  -> [all x [all y [[[p [e x y]] & [p x]] => [p y]]]])       

(define yqf
  {--> prop}
   -> [all x [all y [all z [p [e [e x y] [e [e x z] [e z y]]]]]]])
   
(define ec   
  {--> prop}
   -> [[[p [e x x]] & [p [e [e x y] [e y x]]]] 
                               & [p [e [e x y] [e [e y z] [e x z]]]]]) 
                               
(kb-> [(mp) (yqf)])

(<-kb (ec))
run time: 0.03125 secs
29244 inferences, equality = false
depth = 13, complexity = -1, timeout = 60 secs
true        
*****************************************************************  
Step 1

? (((p (e x x)) & (p (e (e x y) (e y x)))) & (p (e (e x y) (e (e y z) (e x z)))))


> revsk
=============================
Step 2

? (((p (e x x)) & (p (e (e x y) (e y x)))) & (p (e (e x y) (e (e y z) (e x z)))))


> &r
|=============================
|Step 3
|
|? ((p (e x x)) & (p (e (e x y) (e y x))))
|
|
|> &r
||=============================
||Step 4
||
||? (p (e x x))
||
||
||> hypdisj
||=============================
||Step 5
||
||? (p (e x x))
||
||
||> ((p X) <-- (p (e Y X)) (p Y))
|||=============================
|||Step 6
|||
|||? (p (e Var375 (e x x)))
|||
|||
|||> ((p X) <-- (p (e Y X)) (p Y))
||||=============================
||||Step 7
||||
||||? (p (e Var378 (e Var375 (e x x))))
||||
||||
||||> ((p X) <-- (p (e Y X)) (p Y))
|||||=============================
|||||Step 8
|||||
|||||? (p (e Var381 (e Var378 (e Var375 (e x x)))))
|||||
|||||
|||||> ((p X) <-- (p (e Y X)) (p Y))
||||||=============================
||||||Step 9
||||||
||||||? (p (e Var384 (e Var381 (e Var378 (e Var375 (e x x))))))
||||||
||||||
||||||> ((p X) <-- (p (e Y X)) (p Y))
|||||||=============================
|||||||Step 10
|||||||
|||||||? (p (e (e Var392 (e Var378 (e Var375 (e x x)))) (e (e Var392 Var381) (e Var381 (e Var378 (e Var375 (e x x)))))))
|||||||
|||||||
|||||||> ((p (e (e X Z) (e (e X Y) (e Y Z)))) <--)
||||||=============================
||||||Step 11
||||||
||||||? (p (e (e Var398 (e x x)) (e (e Var398 Var375) (e Var375 (e x x)))))
||||||
||||||
||||||> ((p (e (e X Z) (e (e X Y) (e Y Z)))) <--)
|||||=============================
|||||Step 12
|||||
|||||? (p (e (e Var402 (e x x)) (e (e Var402 Var404) (e Var404 (e x x)))))
|||||
|||||
|||||> ((p (e (e X Z) (e (e X Y) (e Y Z)))) <--)
||||=============================
||||Step 13
||||
||||? (p (e (e Var402 Var404) (e Var404 (e x x))))
||||
||||
||||> ((p X) <-- (p (e Y X)) (p Y))
|||||=============================
|||||Step 14
|||||
|||||? (p (e Var408 (e (e Var402 Var404) (e Var404 (e x x)))))
|||||
|||||
|||||> ((p X) <-- (p (e Y X)) (p Y))
||||||=============================
||||||Step 15
||||||
||||||? (p (e (e Var416 (e Var404 (e x x))) (e (e Var416 (e Var402 Var404)) (e (e Var402 Var404) (e Var404 (e x x))))))
||||||
||||||
||||||> ((p (e (e X Z) (e (e X Y) (e Y Z)))) <--)
|||||=============================
|||||Step 16
|||||
|||||? (p (e (e Var422 x) (e (e Var422 x) (e x x))))
|||||
|||||
|||||> ((p (e (e X Z) (e (e X Y) (e Y Z)))) <--)
||||=============================
||||Step 17
||||
||||? (p (e (e Var426 x) (e (e Var426 Var426) (e Var426 x))))
||||
||||
||||> ((p (e (e X Z) (e (e X Y) (e Y Z)))) <--)
|||=============================
|||Step 18
|||
|||? (p (e (e Var430 Var430) (e (e Var430 Var432) (e Var432 Var430))))
|||
|||
|||> ((p (e (e X Z) (e (e X Y) (e Y Z)))) <--)
||=============================
||Step 19
||
||? (p (e (e Var430 Var432) (e Var432 Var430)))
||
||
||> ((p X) <-- (p (e Y X)) (p Y))
|||=============================
|||Step 20
|||
|||? (p (e (e Var430 Var430) (e (e Var430 Var432) (e Var432 Var430))))
|||
|||
|||> ((p (e (e X Z) (e (e X Y) (e Y Z)))) <--)
||=============================
||Step 21
||
||? (p (e Var430 Var430))
||
||
||> ((p X) <-- (p (e Y X)) (p Y))
|||=============================
|||Step 22
|||
|||? (p (e (e Var448 Var448) (e (e Var448 Var448) (e Var448 Var448))))
|||
|||
|||> ((p (e (e X Z) (e (e X Y) (e Y Z)))) <--)
||=============================
||Step 23
||
||? (p (e Var448 Var448))
||
||
||> ((p X) <-- (p (e Y X)) (p Y))
|||=============================
|||Step 24
|||
|||? (p (e Var452 (e Var448 Var448)))
|||
|||
|||> ((p X) <-- (p (e Y X)) (p Y))
||||=============================
||||Step 25
||||
||||? (p (e (e Var460 Var448) (e (e Var460 Var448) (e Var448 Var448))))
||||
||||
||||> ((p (e (e X Z) (e (e X Y) (e Y Z)))) <--)
|||=============================
|||Step 26
|||
|||? (p (e (e Var466 Var469) (e (e Var466 Var468) (e Var468 Var469))))
|||
|||
|||> ((p (e (e X Z) (e (e X Y) (e Y Z)))) <--)
||=============================
||Step 27
||
||? (p (e (e Var466 Var469) (e (e Var466 Var468) (e Var468 Var469))))
||
||
||> ((p (e (e X Z) (e (e X Y) (e Y Z)))) <--)
|=============================
|Step 28
|
|? (p (e (e x y) (e y x)))
|
|
|> hypdisj
|=============================
|Step 29
|
|? (p (e (e x y) (e y x)))
|
|
|> ((p X) <-- (p (e Y X)) (p Y))
||=============================
||Step 30
||
||? (p (e Var478 (e (e x y) (e y x))))
||
||
||> ((p X) <-- (p (e Y X)) (p Y))
|||=============================
|||Step 31
|||
|||? (p (e Var481 (e Var478 (e (e x y) (e y x)))))
|||
|||
|||> ((p X) <-- (p (e Y X)) (p Y))
||||=============================
||||Step 32
||||
||||? (p (e (e Var489 (e (e x y) (e y x))) (e (e Var489 Var478) (e Var478 (e (e x y) (e y x))))))
||||
||||
||||> ((p (e (e X Z) (e (e X Y) (e Y Z)))) <--)
|||=============================
|||Step 33
|||
|||? (p (e (e x x) (e (e x y) (e y x))))
|||
|||
|||> ((p (e (e X Z) (e (e X Y) (e Y Z)))) <--)
||=============================
||Step 34
||
||? (p (e (e x x) (e (e x Var499) (e Var499 x))))
||
||
||> ((p (e (e X Z) (e (e X Y) (e Y Z)))) <--)
|=============================
|Step 35
|
|? (p (e (e x Var499) (e Var499 x)))
|
|
|> ((p X) <-- (p (e Y X)) (p Y))
||=============================
||Step 36
||
||? (p (e Var503 (e (e x Var499) (e Var499 x))))
||
||
||> ((p X) <-- (p (e Y X)) (p Y))
|||=============================
|||Step 37
|||
|||? (p (e Var506 (e Var503 (e (e x Var499) (e Var499 x)))))
|||
|||
|||> ((p X) <-- (p (e Y X)) (p Y))
||||=============================
||||Step 38
||||
||||? (p (e Var509 (e Var506 (e Var503 (e (e x Var499) (e Var499 x))))))
||||
||||
||||> ((p X) <-- (p (e Y X)) (p Y))
|||||=============================
|||||Step 39
|||||
|||||? (p (e (e Var517 (e Var503 (e (e x Var499) (e Var499 x)))) (e (e Var517 Var506) (e Var506 (e Var503 (e (e x Var499) (e Var499 x)))))))
|||||
|||||
|||||> ((p (e (e X Z) (e (e X Y) (e Y Z)))) <--)
||||=============================
||||Step 40
||||
||||? (p (e (e Var523 (e Var499 x)) (e (e Var523 (e x Var499)) (e (e x Var499) (e Var499 x)))))
||||
||||
||||> ((p (e (e X Z) (e (e X Y) (e Y Z)))) <--)
|||=============================
|||Step 41
|||
|||? (p (e (e Var523 (e Var499 x)) Var506))
|||
|||
|||> ((p X) <-- (p (e Y X)) (p Y))
||||=============================
||||Step 42
||||
||||? (p (e (e Var523 Var533) (e (e Var523 (e Var499 x)) (e (e Var499 x) Var533))))
||||
||||
||||> ((p (e (e X Z) (e (e X Y) (e Y Z)))) <--)
|||=============================
|||Step 43
|||
|||? (p (e (e Var538 Var541) (e (e Var538 Var540) (e Var540 Var541))))
|||
|||
|||> ((p (e (e X Z) (e (e X Y) (e Y Z)))) <--)
||=============================
||Step 44
||
||? (p (e (e Var538 x) (e (e Var538 Var540) (e Var540 x))))
||
||
||> ((p (e (e X Z) (e (e X Y) (e Y Z)))) <--)
|=============================
|Step 45
|
|? (p (e (e Var538 x) (e x Var538)))
|
|
|> ((p X) <-- (p (e Y X)) (p Y))
||=============================
||Step 46
||
||? (p (e (e Var538 Var538) (e (e Var538 x) (e x Var538))))
||
||
||> ((p (e (e X Z) (e (e X Y) (e Y Z)))) <--)
|=============================
|Step 47
|
|? (p (e Var538 Var538))
|
|
|> ((p X) <-- (p (e Y X)) (p Y))
||=============================
||Step 48
||
||? (p (e Var553 (e Var538 Var538)))
||
||
||> ((p X) <-- (p (e Y X)) (p Y))
|||=============================
|||Step 49
|||
|||? (p (e (e Var561 Var538) (e (e Var561 Var538) (e Var538 Var538))))
|||
|||
|||> ((p (e (e X Z) (e (e X Y) (e Y Z)))) <--)
||=============================
||Step 50
||
||? (p (e (e Var567 Var570) (e (e Var567 Var569) (e Var569 Var570))))
||
||
||> ((p (e (e X Z) (e (e X Y) (e Y Z)))) <--)
|=============================
|Step 51
|
|? (p (e (e Var567 Var570) (e (e Var567 Var569) (e Var569 Var570))))
|
|
|> ((p (e (e X Z) (e (e X Y) (e Y Z)))) <--)
=============================
Step 52

? (p (e (e x y) (e (e y z) (e x z))))


> hypdisj
=============================
Step 53

? (p (e (e x y) (e (e y z) (e x z))))


> ((p X) <-- (p (e Y X)) (p Y))
|=============================
|Step 54
|
|? (p (e Var579 (e (e x y) (e (e y z) (e x z)))))
|
|
|> ((p X) <-- (p (e Y X)) (p Y))
||=============================
||Step 55
||
||? (p (e Var582 (e Var579 (e (e x y) (e (e y z) (e x z))))))
||
||
||> ((p X) <-- (p (e Y X)) (p Y))
|||=============================
|||Step 56
|||
|||? (p (e Var585 (e Var582 (e Var579 (e (e x y) (e (e y z) (e x z)))))))
|||
|||
|||> ((p X) <-- (p (e Y X)) (p Y))
||||=============================
||||Step 57
||||
||||? (p (e Var588 (e Var585 (e Var582 (e Var579 (e (e x y) (e (e y z) (e x z))))))))
||||
||||
||||> ((p X) <-- (p (e Y X)) (p Y))
|||||=============================
|||||Step 58
|||||
|||||? (p (e (e Var596 (e Var582 (e Var579 (e (e x y) (e (e y z) (e x z)))))) (e (e Var596 Var585) (e Var585 (e Var582 (e Var579 (e (e x y) (e (e y z) (e x z)))))))))
|||||
|||||
|||||> ((p (e (e X Z) (e (e X Y) (e Y Z)))) <--)
||||=============================
||||Step 59
||||
||||? (p (e (e Var602 (e (e x y) (e (e y z) (e x z)))) (e (e Var602 Var579) (e Var579 (e (e x y) (e (e y z) (e x z)))))))
||||
||||
||||> ((p (e (e X Z) (e (e X Y) (e Y Z)))) <--)
|||=============================
|||Step 60
|||
|||? (p (e (e Var602 (e (e x y) (e (e y z) (e x z)))) Var585))
|||
|||
|||> ((p X) <-- (p (e Y X)) (p Y))
||||=============================
||||Step 61
||||
||||? (p (e (e Var602 Var612) (e (e Var602 (e (e x y) (e (e y z) (e x z)))) (e (e (e x y) (e (e y z) (e x z))) Var612))))
||||
||||
||||> ((p (e (e X Z) (e (e X Y) (e Y Z)))) <--)
|||=============================
|||Step 62
|||
|||? (p (e (e Var617 Var620) (e (e Var617 Var619) (e Var619 Var620))))
|||
|||
|||> ((p (e (e X Z) (e (e X Y) (e Y Z)))) <--)
||=============================
||Step 63
||
||? (p (e (e (e x y) (e (e y z) (e x z))) (e (e (e x y) Var619) (e Var619 (e (e y z) (e x z))))))
||
||
||> ((p (e (e X Z) (e (e X Y) (e Y Z)))) <--)
|=============================
|Step 64
|
|? (p (e (e (e x y) (e (e y z) (e x z))) Var579))
|
|
|> ((p X) <-- (p (e Y X)) (p Y))
||=============================
||Step 65
||
||? (p (e Var625 (e (e (e x y) (e (e y z) (e x z))) Var579)))
||
||
||> ((p X) <-- (p (e Y X)) (p Y))
|||=============================
|||Step 66
|||
|||? (p (e Var628 (e Var625 (e (e (e x y) (e (e y z) (e x z))) Var579))))
|||
|||
|||> ((p X) <-- (p (e Y X)) (p Y))
||||=============================
||||Step 67
||||
||||? (p (e (e Var636 (e (e (e x y) (e (e y z) (e x z))) Var579)) (e (e Var636 Var625) (e Var625 (e (e (e x y) (e (e y z) (e x z))) Var579)))))
||||
||||
||||> ((p (e (e X Z) (e (e X Y) (e Y Z)))) <--)
|||=============================
|||Step 68
|||
|||? (p (e (e (e x y) Var643) (e (e (e x y) (e (e y z) (e x z))) (e (e (e y z) (e x z)) Var643))))
|||
|||
|||> ((p (e (e X Z) (e (e X Y) (e Y Z)))) <--)
||=============================
||Step 69
||
||? (p (e (e (e x y) Var649) (e (e (e x y) Var648) (e Var648 Var649))))
||
||
||> ((p (e (e X Z) (e (e X Y) (e Y Z)))) <--)
|=============================
|Step 70
|
|? (p (e (e (e x y) (e (e x y) Var654)) (e (e (e x y) Var654) (e Var654 (e (e x y) Var654)))))
|
|
|> ((p (e (e X Z) (e (e X Y) (e Y Z)))) <--)
=============================
Step 71

? (p (e (e (e y z) (e x z)) (e Var654 (e (e x y) Var654))))


> ((p X) <-- (p (e Y X)) (p Y))
|=============================
|Step 72
|
|? (p (e Var658 (e (e (e y z) (e x z)) (e Var654 (e (e x y) Var654)))))
|
|
|> ((p X) <-- (p (e Y X)) (p Y))
||=============================
||Step 73
||
||? (p (e (e Var666 (e Var654 (e (e x y) Var654))) (e (e Var666 (e (e y z) (e x z))) (e (e (e y z) (e x z)) (e Var654 (e (e x y) Var654))))))
||
||
||> ((p (e (e X Z) (e (e X Y) (e Y Z)))) <--)
|=============================
|Step 74
|
|? (p (e Var666 (e Var654 (e (e x y) Var654))))
|
|
|> ((p X) <-- (p (e Y X)) (p Y))
||=============================
||Step 75
||
||? (p (e (e Var675 (e (e x y) Var654)) (e (e Var675 Var654) (e Var654 (e (e x y) Var654)))))
||
||
||> ((p (e (e X Z) (e (e X Y) (e Y Z)))) <--)
|=============================
|Step 76
|
|? (p (e (e x Var682) (e (e x y) (e y Var682))))
|
|
|> ((p (e (e X Z) (e (e X Y) (e Y Z)))) <--)
=============================
Step 77

? (p (e (e (e x Var682) (e y Var682)) (e (e y z) (e x z))))


> ((p X) <-- (p (e Y X)) (p Y))
|=============================
|Step 78
|
|? (p (e Var685 (e (e (e x Var682) (e y Var682)) (e (e y z) (e x z)))))
|
|
|> ((p X) <-- (p (e Y X)) (p Y))
||=============================
||Step 79
||
||? (p (e Var688 (e Var685 (e (e (e x Var682) (e y Var682)) (e (e y z) (e x z))))))
||
||
||> ((p X) <-- (p (e Y X)) (p Y))
|||=============================
|||Step 80
|||
|||? (p (e (e Var696 (e (e (e x Var682) (e y Var682)) (e (e y z) (e x z)))) (e (e Var696 Var685) (e Var685 (e (e (e x Var682) (e y Var682)) (e (e y z) (e x z)))))))
|||
|||
|||> ((p (e (e X Z) (e (e X Y) (e Y Z)))) <--)
||=============================
||Step 81
||
||? (p (e (e (e x z) (e x z)) (e (e (e x z) (e y z)) (e (e y z) (e x z)))))
||
||
||> ((p (e (e X Z) (e (e X Y) (e Y Z)))) <--)
|=============================
|Step 82
|
|? (p (e (e (e x z) (e x z)) Var685))
|
|
|> ((p X) <-- (p (e Y X)) (p Y))
||=============================
||Step 83
||
||? (p (e (e (e x z) Var710) (e (e (e x z) (e x z)) (e (e x z) Var710))))
||
||
||> ((p (e (e X Z) (e (e X Y) (e Y Z)))) <--)
|=============================
|Step 84
|
|? (p (e (e x z) (e (e x Var715) (e Var715 z))))
|
|
|> ((p (e (e X Z) (e (e X Y) (e Y Z)))) <--)
=============================
Step 85

? (p (e (e x z) (e (e x Var715) (e Var715 z))))


> ((p (e (e X Z) (e (e X Y) (e Y Z)))) <--)
